Iof proof for Lemma nat ind tp:
1. P :
{k}
2. P(0)
3.
i:
. P(i - 1) 
P(i)
4. 0
0
P(0)
by ((Thin (-1))
CollapseTHEN (AddHiddenLabel `basecase`))
C1: .....basecase..... NILNIL
C1: 3. i:. P(i - 1) P(i)
C1: P(0)
C.| 9,38 |
{k}
i:. P(i - 1) P(i)
0
P(0)
by ((Thin (-1))
CollapseTHEN (AddHiddenLabel `basecase`))
C1: .....basecase..... NILNIL
C1: 3. i:. P(i - 1) P(i)
C1: P(0)
C.